#!/usr/bin/gosh
;; -*- scheme -*-
(use srfi-1)
(use util.combinations)
(use gauche.process)

(define (main args)
    (if (not (= (length args) 3))
        (begin
         (print "Usage: " *program-name* " problem answer")
         0)
        (let ((csp (cadr args)))
          (case (read-answer (caddr args))
            ((UNSAT)   (print "Can not validate: UNSAT.") 0)
            ((UNKNOWN) (print "Can not validate: UNKNOWN") 0)
            ((SAT)
             (let ((with-csp (if (#/\.xml$/ csp)
                                 (cut with-input-from-process
                                      `(,(string-append (rxmatch->string "^(.+/)" *program-name*)
                                                       "xml2csp") ,csp) <>)
                                 (cut with-input-from-file csp <>))))
               (with-csp
                   (cut port-for-each
                        (lambda (exp)
                          (unless (eval exp (interaction-environment))
                            (print "Error: " exp " is violated.")))
                        read)))
             0)
            (else (print "Invalid answer."))))))

(define (read-answer ans)
    (let ((*RESULT* #f))
      (with-input-from-file ans
        (cut port-for-each
             (lambda (line)
               (rxmatch-cond
                (test (equal? "s UNSATISFIABLE" line)
                      (set! *RESULT* 'UNSAT))
                (test (equal? "s SATISFIABLE" line)
                      (set! *RESULT* 'SAT))
                (test (equal? "s UNKNOWN" line)
                      (set! *RESULT* 'UNKNOWN))
                ((rxmatch #/^a ([^\s]+)\s+([^\s]+)$/ line)
                 (#f var val)
                 (eval `(define ,(string->symbol var)
                            ,(if (#/^-?\d+$/ val)
                                 (string->number val)
                                 (eval (string->symbol val)
                                       (interaction-environment))))
                       (interaction-environment)))))
             read-line))
      *RESULT*))

(define-macro (domain name lb . args)
    (let-optionals*
     args ((ub '()))
     (cond ((integer? ub) `(define ,name (quote ((,lb ,ub)))))
           ((integer? lb) `(define ,name (quote (,lb))))
           (else `(define ,name (quote ,lb))))))

(define (var-in-domain var lst)
    (any (lambda (hd)
           (if (integer? hd)
               (= var hd)
               (and (<= (car hd) var)
                    (<= var (cadr hd)))))
         lst))

(define-macro (int var lb . args)
    (let-optionals*
     args ((ub '()))
     (cond ((integer? ub)
            `(and (<= ,lb ,var) (<= ,var ,ub)))
           ((integer? lb) `(= ,var ,lb))
           ((list? lb)
            `(var-in-domain ,var (quote ,lb)))
           (else `(var-in-domain ,var ,lb)))))

(define (bool p) #t)

(define neg -)
(define add +)
(define sub -)
(define mul *)
(define div quotient)
(define / quotient)
(define mod modulo)
(define %   modulo)
;; (define pow xxx)

(define-macro (relation name arity relbody)
    (let* ((rel (car relbody))
           (args (map gensym (map number->string (iota arity))))
           (pts (cdr relbody))
           (sup `(any (cut list= = (list ,@args) <>)
                      (quote ,pts))))
      `(define (,name ,@args)
           ,(if (equal? rel 'supports)
                sup
                `(not ,sup)))))

(define-macro (predicate args predbody)
    `(define ,args ,predbody))

(define ! not)
(define && and)
(define || or)
(define (imp lhs rhs) (or (not lhs) rhs))
(define => imp)
(define (xor p q)
    (or (and p (not q))
        (and (not p) q)))
(define (iff lhs rhs)
    (and (=> lhs rhs)
         (=> rhs lhs)))
(define true #t)
(define false #f)
(define eq =)
(define (ne x y) (not (= x y)))
(define != ne)
(define le <=)
(define lt <)
(define ge >=)
(define gt >)

(define-macro (alldifferent term . args)
  (if (null? args)
      `(every (cut apply ne <>)
              (combinations (list ,@term) 2))
      `(alldifferent ,(cons term args))))
(define-macro (weightedsum pairs op term)
    `(,op (apply + (map (cut apply * <>)
                        (list ,@(map (lambda (x) `(list ,@x)) pairs)))) ,term))
(define-macro (cumulative tasks_ limit)
    (let* ((origin (cut ref <> 0))
           (duration (cut ref <> 1))
           (end (cut ref <> 2))
           (height (cut ref <> 3))
           (lb (gensym))
           (ub (gensym))
           (value (gensym))
           (it (gensym))
           (tasks (map (lambda (x)
                         (cond ((equal? (origin x) 'nil)
                                `(list (- ,(end x) ,(duration x))
                                       ,(duration x) ,(end x) ,(height x)))
                               ((equal? (duration x) 'nil)
                                `(list ,(origin x)
                                       (- ,(end x) ,(origin x))
                                       ,(end x) ,(height x)))
                               ((equal? (end x) 'nil)
                                `(list ,(origin x) ,(duration x)
                                       (+ ,(origin x) ,(duration x))
                                       ,(height x)))
                               (else `(list ,@x)))) tasks_)))
      `(let ((,lb (apply min (map (cut ref <> 0) (list ,@tasks))))
             (,ub (apply max (map (lambda (,it) (- (ref ,it 2) 1))
                                  (list ,@tasks)))))
         (and (every (lambda (,it)
                           (equal? (+ (ref ,it 0) (ref ,it 1))
                                   (ref ,it 2)))
                     (list ,@tasks))
              (every (lambda (,value)
                       (<= (apply +
                                  (map (cut ref <> 3)
                                       (filter (lambda (,it)
                                                 (and (<= (ref ,it 0) ,value)
                                                      (> (ref ,it 2) ,value)))
                                               (list ,@tasks))))
                           ,limit))
                     (iota (+ (- ,ub ,lb) 1) ,lb 1))))))
(define-macro (element idx terms value)
    `(= (values-ref (list ,@terms) (- ,idx 1)) ,value))
(define-macro (disjunctive tasks)
    (let ((durs (gensym))
          (x (gensym))
          (y (gensym)))
      `(let ((,durs (sort-by (filter (lambda (,x) (positive? (cadr ,x)))
                                     (list ,@tasks)) car)))
         (apply and
                (map (lambda (,x ,y) (<= (apply + ,x) (car ,y)))
                     ,durs (cdr ,durs))))))
(define-macro (lex_less vec1 vec2)
    `(apply and (map < (list ,@vec1) (list ,@vec2))))
(define-macro (lex_lesseq vec1 vec2)
    `(if (null? (list ,@vec1))
         #t
         (apply and (map <= (list ,@vec1) (list ,@vec2)))))
(define-macro (nvalue term terms)
    `(= ,term (length (fold (lambda (a r)
                              (if (member a r)
                                  r
                                  (cons a r)))
                            '() (list ,@terms)))))
(define-macro (global_cardinality terms cards)
    `(if (null? (list ,@cards))
         #t
         (apply and (map (lambda (c)
                           (= (cadr c)
                              (count (cut = <> (car c))
                                     (list ,@terms))))
                         (list ,@cards)))))
(define-macro (global_cardinality_with_costs terms cards tables costs)
    `(if (null? (list ,@cards))
         (= ,costs 0)
         (and
          (global_cardinality ,terms ,cards)
          (let ((vals (map-with-index
                       (lambda (i x)
                         (cons i (find-index
                                  (lambda (p)
                                    (= x (car p))) (list ,@cards))))
                       (list ,@terms))))
            (= ,costs
               (apply + (map (lambda (x)
                               (ref (find (lambda (tbl)
                                            (and (= (+ (car x) 1)
                                                    (ref tbl 0))
                                                 (= (+ (cdr x) 1)
                                                    (ref tbl 1))))
                                          (list ,@tables)) 2))
                             vals)))))))
(define-macro (count value terms op term)
    `(,op (fold (lambda (acc x)
                  (if (= x ,value)
                      (+ 1 acc) acc)) 0 (list ,@terms))
          ,term))
(define (objective goal name)
    #t)
